(declare-const a String)
(declare-const b String)
(declare-const c String)
(declare-const d String)
(declare-const e String)
(declare-const f Bool)
(assert (= f (and (= "sqs" a))))
(declare-const g Bool)
(assert (= g (and (= c "aws") (= e "") (= b "111144448888") (str.in_re d (re.++ (str.to_re "ab") (str.to_re "bb") (re.* re.allchar) (str.to_re "b"))))))
(declare-const h Bool)
(assert (= h (and f g)))
(declare-const k Bool)
(assert (= k true h))
(declare-const i Bool)
(assert (= i (not k)))
(declare-const j Bool)
(assert (= j (= "" a)))
(declare-const l Bool)
(assert (= l (and (= c "aws") (= b "111144448888") (str.in_re d (re.++ (str.to_re "a") (re.* re.allchar) (str.to_re "b") (re.* re.allchar) (str.to_re "b"))))))
(declare-const m Bool)
(assert (= m l))
(declare-const n Bool)
(assert (= n m))
(assert (not n))
(assert (not (str.contains e ":")))
(check-sat)
